Search for: All records

The determinization of a nondeterministic Büchi automaton (NBA) is a fundamental construction of automata theory, with applications to probabilistic verification and reactive synthesis. The standard determinization constructions, such as the ones based on the Safra-Piterman’s approach, work on the whole NBA. In this work we propose a divide-and-conquer determinization approach. To this end, we first classify the strongly connected components (SCCs) of the given NBA as inherently weak, deterministic accepting, and nondeterministic accepting. We then present how to determinize each type of SCC independently from the others; this results in an easier handling of the determinization algorithm that takes advantage of the structure of that SCC. Once all SCCs have been determinized, we show how to compose them so to obtain the final equivalent deterministic Emerson-Lei automaton, which can be converted into a deterministic Rabin automaton without blow-up of states and transitions. We implement our algorithm in our tool COLA and empirically evaluate COLA with the state-of-the-art tools Spot and Owl on a large set of benchmarks from the literature. The experimental results show that our prototype COLA outperforms Spot and Owl regarding the number of states and transitions. 

Adding a cationic helper lipid to a lipid nanoparticle (LNP) can increase lung delivery and decrease liver delivery. However, it remains unclear whether charge-dependent tropism is universal or, alternatively, whether it depends on the component that is charged. Here, we report evidence that cationic cholesterol-dependent tropism can differ from cationic helper lipid-dependent tropism. By testing how 196 LNPs delivered mRNA to 22 cell types, we found that charged cholesterols led to a different lung:liver delivery ratio than charged helper lipids. We also found that combining cationic cholesterol with a cationic helper lipid led to mRNA delivery in the heart as well as several lung cell types, including stem cell-like populations. These data highlight the utility of exploring charge-dependent LNP tropism.